Nuprl Lemma : as_strong_wf 4,23

T:Type, QP:(TProp). P as strong as Q   Prop 
latex


DefinitionsP as strong as Q , x:AB(x), P  Q, Prop, t  T

origin